r:Rng. r+gp  AbGrp 

latex

Up	rings 1
Definitions of Statement	Rng, r+gp
Definitions	t  T, x:A. B(x), AbGrp, t.2, t.1, *, r+gp, |g|, Comm(T;op), Mon, , Group{i}, Rng
Lemmas	rng wf, grp op wf, grp car wf, comm wf, add grp of rng wf a, rng car wf, rng plus comm